<html>
<head><meta charset="utf-8"><title>Quantifier elimination for HRTBs · t-compiler/wg-polonius · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/index.html">t-compiler/wg-polonius</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html">Quantifier elimination for HRTBs</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="237573768"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237573768" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Dylan MacKenzie (ecstatic-morse) <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237573768">(May 05 2021 at 21:50)</a>:</h4>
<p>Howdy <span class="user-group-mention" data-user-group-id="1184">@WG-polonius</span>. I recently published a <a href="https://ecstaticmorse.net/posts/quantifier-elimination/">blog post</a> describing a strategy for reducing higher-ranked trait bounds to unquantified region constraints. It's a response to <a href="https://smallcultfollowing.com/babysteps/blog/2019/01/21/hereditary-harrop-region-constraints/">"Polonius and the case of the hereditary harrop predicate"</a>, although that post is quite old and may not reflect the current thinking around HRTBs. Even if some or all of my ideas are already known to the Polonius team, the blog post may still be useful since I was able to find relevant prior art that I haven't seen discussed anywhere, specifically some results on precedence constraints in atomic Boolean algebras showing a limit on how powerful our region logic can be while remaining decidable.</p>
<p>I had these ideas back when I was making some trivial fixes to get up to speed with Polonius. I was hesitant to share them at the time because I was both unsure about their novelty and worried I had made a trivial mistake somewhere: I'm an amateur mathematician and a lousy one at that. I had planned to start with a more concrete proposal about using a variant of the SSA transformation to speed up computing borrow errors, but that idea turned out to have a fatal flaw. Partly because of that negative result and partly because of some health problems, I stopped working on Polonius in my free time. Now that I'm feeling better, however, it seemed wasteful not to publish my results despite the possibility of a minor embarrassment.</p>



<a name="237574073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237574073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237574073">(May 05 2021 at 21:53)</a>:</h4>
<p><span class="user-mention" data-user-id="118594">@ecstatic-morse</span> hey Dylan &lt;3</p>



<a name="237574211"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237574211" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237574211">(May 05 2021 at 21:55)</a>:</h4>
<p>this looks lovely I'll read it carefully; hope everything's better health-wise</p>



<a name="237574368"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237574368" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237574368">(May 05 2021 at 21:56)</a>:</h4>
<p>from the top of my head, your mentioning the variant of the SSA transformation, reminds me, IIRC, of arielb talking about Graph SSA for easier borrow checking <span aria-label="thinking" class="emoji emoji-1f914" role="img" title="thinking">:thinking:</span></p>



<a name="237574499"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237574499" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237574499">(May 05 2021 at 21:58)</a>:</h4>
<p>(but maybe I'm conflating this with their Ref 2 Φ model)</p>



<a name="237574810"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237574810" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237574810">(May 05 2021 at 22:00)</a>:</h4>
<p>it would be cool if <span class="user-mention" data-user-id="116009">@nikomatsakis</span> had an update to that plan to share btw ? <span aria-label="pray" class="emoji emoji-1f64f" role="img" title="pray">:pray:</span>  since chalk has made a lot of progress since then (and they may have some of those ideas fresh from the recent rust verification workshop)</p>



<a name="237575062"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237575062" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Dylan MacKenzie (ecstatic-morse) <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237575062">(May 05 2021 at 22:03)</a>:</h4>
<p>Yeah, I've seen an IRLO thread where  they discussed SSA, although my idea's a bit different. I'm hoping to write it up and let others take a crack at fixing it.</p>



<a name="237575242"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237575242" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237575242">(May 05 2021 at 22:04)</a>:</h4>
<p>the Revesz paper also looks very interesting, thanks a bunch for writing this up</p>



<a name="237578079"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237578079" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237578079">(May 05 2021 at 22:35)</a>:</h4>
<p>(maybe the algorithm they had in mind isn't exactly the same as yours, but I agree that it does sound a lot like the discussions I remember from Niko &amp; wg-traits, that chalk would handle the quantifiers from higher-ranked constraints and emit quantifier-free constraints for polonius to solve ; maybe it was also because this would be needed during trait-solving, rather than a concern solely about borrow checking ?)</p>



<a name="237586808"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237586808" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237586808">(May 06 2021 at 00:15)</a>:</h4>
<p>(or maybe operational concerns on how to apply this within existing datalog engines ? hopefully they'll explain :)</p>



<a name="237586854"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237586854" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237586854">(May 06 2021 at 00:16)</a>:</h4>
<p>what an enjoyable read</p>



<a name="237586858"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237586858" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237586858">(May 06 2021 at 00:16)</a>:</h4>
<p>I believe that lower bounds on universal quantification are similarly eliminated in current NLLs, <code>for&lt;'a&gt; 'b: 'a</code> being eliminated as <code>'b: 'static</code>. Interestingly, this substitution does show up sometimes in user code as an unexpected <code>'static</code> bound surfaced in error messages and diagnostics, and surprises them of course.</p>



<a name="237586894"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237586894" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237586894">(May 06 2021 at 00:16)</a>:</h4>
<p>I'm not exactly sure what Niko had in mind when they mentioned implication as a richer constraint we'll eventually need, but I <em>believe</em> that disjunction would be used for the now-existing <a href="https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference/member_constraints.html">member constraints</a> that arise from <code>impl Trait</code>, and the <code>async fn</code> desugaring. As you mention, I'm not sure either whether quantifiers are allowed there (I'd be surprised), so maybe indeed we could allow disjunction only outside of quantifiers.</p>



<a name="237587216"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237587216" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237587216">(May 06 2021 at 00:21)</a>:</h4>
<p>again, lovely post, thanks for writing it. I'm excited for more :)</p>



<a name="237729161"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237729161" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Dylan MacKenzie (ecstatic-morse) <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237729161">(May 06 2021 at 21:05)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116113">lqd</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Quantifier.20elimination.20for.20HRTBs/near/237586858">said</a>:</p>
<blockquote>
<p>I believe that lower bounds on universal quantification are similarly eliminated in current NLLs, <code>for&lt;'a&gt; 'b: 'a</code> being eliminated as <code>'b: 'static</code>. Interestingly, this substitution does show up sometimes in user code as an unexpected <code>'static</code> bound surfaced in error messages and diagnostics, and surprises them of course.</p>
</blockquote>
<p>Yeah, I suspect all of my QE rules already exist somewhere in the NLL implementation, though I wasn't able to find where. NLL also has sets with subset relations, they're just sets of program locations instead of loans, so the QE stuff still applies. At least now there's a long-winded justification for them somewhere <span aria-label="laughing" class="emoji emoji-1f606" role="img" title="laughing">:laughing:</span>.</p>



<a name="237730994"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/237730994" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Dylan MacKenzie (ecstatic-morse) <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#237730994">(May 06 2021 at 21:14)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116113">lqd</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Quantifier.20elimination.20for.20HRTBs/near/237586894">said</a>:</p>
<blockquote>
<p>I'm not exactly sure what Niko had in mind when they mentioned implication as a richer constraint we'll eventually need, but I <em>believe</em> that disjunction would be used for the now-existing <a href="https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference/member_constraints.html">member constraints</a> that arise from <code>impl Trait</code>, and the <code>async fn</code> desugaring. As you mention, I'm not sure either whether quantifiers are allowed there (I'd be surprised), so maybe indeed we could allow disjunction only outside of quantifiers.</p>
</blockquote>
<p>Thanks. That's good to know. AFAICT, the main problem is disjunction inside a universal quantifier. We don't have to deal with negation, so we can convert to disjunctive normal form using only the distributive law, and existential quantifiers distribute over disjunction. I don't know how to prove statements like <code>forall&lt;'x&gt; { 'x : 'a || 'a : 'x }</code>, however. It might not be an issue like you said.</p>



<a name="239090398"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/239090398" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#239090398">(May 17 2021 at 13:40)</a>:</h4>
<p>so <span class="user-mention" data-user-id="118594">@ecstatic-morse</span> I read your post btw :)</p>



<a name="239090402"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/239090402" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#239090402">(May 17 2021 at 13:40)</a>:</h4>
<p>I keep meaning to write here!</p>



<a name="239090420"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/239090420" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#239090420">(May 17 2021 at 13:40)</a>:</h4>
<p>tl;dr yes I was aware of that, but it's too simplistic to really work</p>



<a name="239090471"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/239090471" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#239090471">(May 17 2021 at 13:40)</a>:</h4>
<p>I have more thoughts that I've not gotten arond to writing up in blog post form</p>



<a name="239090492"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/239090492" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#239090492">(May 17 2021 at 13:40)</a>:</h4>
<p>though I'm expecting to consult with some folks soon about this very topic!</p>



<a name="239090505"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Quantifier%20elimination%20for%20HRTBs/near/239090505" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Quantifier.20elimination.20for.20HRTBs.html#239090505">(May 17 2021 at 13:40)</a>:</h4>
<p>who have deeper knowledge than me</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>